Iof proof for Lemma lt int eq true elim sqequal:
i, j:
. (i <z j ~ tt) 
(i < j)
by (RepeatFor 2 ((D 0)
THENW ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
T)) (first_tok :t) inil_term)))
)
T1:
T1: 1. i :
T1: 2. j :
T1: (i <z j ~ tt) (i < j)
T.
T